\begin{tabbing}
d{-}machine($i$;$M$;${\it dec}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\langle$${\it dec}$\+
\\[0ex]$,\,$($\lambda$$k$,$v$,$s$,$x$. \=if islocal($k$) $\vee_{2}$ destination(lnk($k$)) = $i$$\rightarrow$ $M$.ef($k$,$x$,$s$,$v$)?$s$($x$)\+
\\[0ex]else $s$($x$) fi)
\-\\[0ex]$,\,$($\lambda$$k$,$v$,$s$. \=if \=islocal($k$) $\vee_{2}$ destination(lnk($k$)) = $i$$\rightarrow$\+\+
\\[0ex]filter($\lambda$$m$.source(mlnk($m$)) = $i$;$M$.sends($k$,$s$,$v$))
\-\\[0ex]else nil fi)$\rangle$
\-\-
\end{tabbing}